$\forall$$T$:Type, ${\it as}$:($T$ List), $R$:($T$$\rightarrow$$T$$\rightarrow$prop\{i:l\}).
\\[0ex]($\forall$$x$:$T$. $\neg$$R$($x$,$x$)) $\Rightarrow$ l{-}ordered($T$; $x$,$y$.$R$($x$,$y$); ${\it as}$) $\Rightarrow$ no\_repeats($T$; ${\it as}$)